singing

And that brings me so we have a we have an inference procedure together with for terminologies

and assertions and concept axioms which now lets us put the whole thing together

make a couple of examples. So for the instance test, which really is concept membership, we can just basically

look, we want to see whether if we have a t-box, say a woman is a person with a Y chromosome and man without,

and we have Tony being a person and Tony having a Y chromosome, we might actually want to find out

whether Tony is an instance not only of person and has Y but also of man. So how do we compute this?

Remember, we have already computed subsumption, which is just by satisfiability. Here we want to say whether

Tony is a man and thus probably a male student and so on.

And so we want to compute the notion of realization, which is putting all the A-box into, in a way, the lowest concepts

they can be. We know that Tony is a man, we can put him into male student, whereas for Terry, where we don't know

whether Terry is male or female, we can just put him or her into the student class.

So there's a couple of things that if we want to compute consistencies and inconsistencies with this algorithm

we just talked about, there's a couple of things that where inconsistencies can come from.

So you can be internally inconsistent, we say. So that would be a case where Tony is a student and at the same time

a non-student. That's inconsistency at the level of an A-box. We have inconsistency with a T-box, say we have a T-box

that says students and professors are disjoined and you have Tony being a student and also a professor.

Without the T-box, this would be perfectly okay. With the T-box, we need the concept axiom in the T-box

that tells us this is not okay because Tony being a student and Tony being a professor violates this concept axiom

which is by the way exactly what our extension to the ALC calculus actually tried to detect.

Then we have the situation where implicit information that is not explicit, so maybe for the A-box we have

Tony who is an object such that all of his grad students are geniuses and Tony is related to Mary

in the has-graduated student relation, so Mary is a grad student of Tony. So you can conclude that Mary must be a genius

because she is a grad student of Tony and therefore she must be a genius because all of his grad students are.

Of course you can take T-box info and actually do this. So here we've basically used A-box information only

but we can also use T-box information for that by just introducing the concept of a content of a happy professor

namely that's a professor who only has geniuses as grad students. So Tony is a content professor who has a grad student

Mary and then we can again find out that Mary is a genius. So these are the kinds of things you get in inference.

So for instance tests and realization we actually need to look at the A-box and the T-box together and we want to see whether an assertion holds here.

And again we're testing A to show, to ask whether A is in phi, we test whether A is in the complement and test that for consistency

together with all the A-box and the T-box information. So what do we do? We need to normalize the A-box with respect to the T-box

that's something we saw earlier meaning in the A-box we replace all the defined constants then we initialize the tableau with the A-box

in negation normal form so that you can actually use it. So if we go back to our example with the happy professor

then we have the T-box that a happy professor is one who has grad students who are geniuses and the A-box is that Tony is a content professor

and has a grad student Mary. So we eliminate the happy professor thing so Tony is a prof who has a grad student

all of whose grad students are geniuses that's the T-box part, Tony has grad Mary is an A-box part. We query whether Mary might not be a genius

and then we start saturating the tableau with the rules from above. This closes and then we know that

Mary is in the concept genius and that allows us and we try that for all possible concepts and if we've tried it for all possible concepts

we know exactly where we want to put Tony and Mary and so on. You can imagine that you don't really actually test all of the concept

but the taxonomy you've computed before is going to play a role here. But essentially you could just go full out

and actually test all of them and then you would have a realization and via the instance test I've shown here.

And that's really all we all you want. Remember you write down knowledge about the world using the ALC language.

That gives us and you write down a T-box. You write down concept definitions.

You write down an A-box and then using the Tableau calculus for ALC.

Here's an example. You can always compute subsumption and realization.

And that gives you a picture like this, which is something you can actually play with and see whether this is the stuff you want.

Turns out that you can write down quite a lot about the world in ALC already.

If you really want to put the whole thing to a test, you want to write down more.

And the semantic web, which kind of uses the whole web as an A-box, this really puts expressivity to the test.

And so all of these ideas from ALC have actually found their way into this semantic web technology, which is what I want to an application that I want to describe next.